////////////////////////////////////////////////////////////////////////////////
// This file is part of the Mist compiler.                                    //
//                                                                            //
// Copyright (C) 2009, 2010 The Mist project                                  //
//                                                                            //
// For a list of contributors, see the COMMITTERS file.                       //
//                                                                            //
// The Mist compiler is free software: you can redistribute it and/or modify  //
// it under the terms of the GNU General Public License as published by       //
// the Free Software Foundation, either version 3 of the License, or          //
// (at your option) any later version.                                        //
//                                                                            //
// The Mist compiler is distributed in the hope that it will be useful,       //
// but WITHOUT ANY WARRANTY; without even the implied warranty of             //
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the              //
// GNU General Public License for more details.                               //
//                                                                            //
// You should have received a copy of the GNU General Public License          //
// in the COPYING file. If not, see <http://www.gnu.org/licenses/>.           //
////////////////////////////////////////////////////////////////////////////////

///
/// \file
/// Contains the implementation of the copy_ast function.
///

#include "copyast.hpp"

////////////////////////////////////////////////////////////////////////////////
// Includes                                                                   //
////////////////////////////////////////////////////////////////////////////////

#include <boost/foreach.hpp>
#define foreach BOOST_FOREACH

#include <stack>
using std::stack;

#include "common/assert.hpp"
#include "common/ptr.hpp"
#include "nodes.hpp"
#include "symbol.hpp"
#include "tree.hpp"
#include "visitor.hpp"

////////////////////////////////////////////////////////////////////////////////
// CopyAstVisitor Class                                                       //
////////////////////////////////////////////////////////////////////////////////

/// Visits the nodes of an abstract syntax sub-tree to deep-copy it.
///
class CopyAstVisitor : public Visitor {
	public:
		
		CopyAstVisitor(map<wptr<Symbol>, sptr<Node> > replacements);
		
		VISIT_FUNCTIONS_FROM( CONCRETE_NODES )
		
		template <class T>
		sptr<T> get_copy_of(wptr<T> node);
		
		template <class T>
		sptr<T> get_copy_of(sptr<T> node);
		
		sptr<Expression> get_translation_of_expression(wptr<Expression> node);
		
		sptr<Type> get_translation_of_type(wptr<Type> node);
	
	private:
		
		stack<sptr<Node> > _current;
		
		map<wptr<Symbol>, sptr<Node> > _replacements;
};

////////////////////////////////////////////////////////////////////////////////
// Function Implementations                                                   //
////////////////////////////////////////////////////////////////////////////////

sptr<Node> copy_ast(wptr<Node> ast, map<wptr<Symbol>, sptr<Node> > replacements, wptr<Symbol> scope) {
	assert(ast);
	
	sptr<CopyAstVisitor> visitor(new CopyAstVisitor(replacements));
	
	sptr<Node> result = visitor->get_copy_of(ast);
	
	result->scope = (scope ? scope : ast->scope());
	
	return result;
}

////////////////////////////////////////////////////////////////////////////////

CopyAstVisitor::CopyAstVisitor(map<wptr<Symbol>, sptr<Node> > replacements) : _replacements(replacements) {
} // intentionally empty

void CopyAstVisitor::visit(wptr<Declarations> node) {
	assert(node);
	
	sptr<Declarations> result = Declarations::construct();
	result->location = node->location;
	
	foreach (wptr<Declaration> decl, node->declarations)
		result->declarations.push_back(get_copy_of(decl));
	
	_current.push(result);
}

void CopyAstVisitor::visit(wptr<AssertionArea> node) {
	assert(node);
	
	sptr<AssertionArea> result = AssertionArea::construct();
	result->location = node->location;
	
	foreach (wptr<Expression> cond, node->conditions)
		result->conditions.insert(get_translation_of_expression(cond));
	
	_current.push(result);
}

void CopyAstVisitor::visit(wptr<IfStatement> node) {
	assert(node);
	
	sptr<IfStatement> result = IfStatement::construct();
	result->location = node->location;
	
	result->condition = get_translation_of_expression(node->condition);
	
	result->thenStatement = get_copy_of(node->thenStatement);
	
	if (node->elseStatement)
		result->elseStatement = get_copy_of(node->elseStatement);
	
	_current.push(result);
}

void CopyAstVisitor::visit(wptr<WhileStatement> node) {
	assert(node);
	
	sptr<WhileStatement> result = WhileStatement::construct();
	result->location = node->location;
	
	result->condition = get_translation_of_expression(node->condition);
	
	foreach (wptr<AssertionArea> inv, node->invariant)
		result->invariant.insert(get_copy_of(inv));
	
	foreach (wptr<Expression> bound, node->bound)
		result->bound.insert(get_translation_of_expression(bound));
	
	foreach (wptr<CompoundStatement> stmt, node->statement)
		result->statement.insert(get_copy_of(stmt));
	
	_current.push(result);
}

void CopyAstVisitor::visit(wptr<ForStatement> node) {
	assert(node);
	
	sptr<ForStatement> result = ForStatement::construct();
	result->location = node->location;
	
	result->iterator = get_copy_of(node->iterator);
	
	result->collection = get_translation_of_expression(node->collection);
	
	foreach (wptr<AssertionArea> inv, node->invariant)
		result->invariant.insert(get_copy_of(inv));
	
	foreach (wptr<CompoundStatement> stmt, node->statement)
		result->statement.insert(get_copy_of(stmt));
	
	_current.push(result);
}

void CopyAstVisitor::visit(wptr<CompoundStatement> node) {
	assert(node);
	
	sptr<CompoundStatement> result = CompoundStatement::construct();
	result->location = node->location;
	
	if (node->name)
		result->name = get_copy_of(node->name);
	
	foreach (wptr<Statement> stmt, node->statements)
		result->statements.push_back(get_copy_of(stmt));
	
	_current.push(result);
}

void CopyAstVisitor::visit(wptr<CppStatement> node) {
	assert(node);
	
	sptr<CppStatement> result = CppStatement::construct(node->code);
	result->location = node->location;
	
	_current.push(result);
}

void CopyAstVisitor::visit(wptr<VariableDeclaration> node) {
	assert(node);
	
	sptr<VariableDeclaration> result = VariableDeclaration::construct();
	result->location = node->location;
	
	result->type = get_translation_of_type(node->type);
	
	foreach (VariableDeclaration::Pair pair, node->pairs) {
		VariableDeclaration::Pair newPair;
		newPair.name = get_copy_of(pair.name);
		if (pair.init)
			newPair.init = get_translation_of_expression(pair.init);
		result->pairs.push_back(newPair);
	}
	
	_current.push(result);
}

void CopyAstVisitor::visit(wptr<TypeDeclaration> node) {
	assert(node);
	
	sptr<TypeDeclaration> result = TypeDeclaration::construct();
	result->location = node->location;
	
	result->name = get_copy_of(node->name);
	
	result->cpp = node->cpp;
	
	result->KeY = node->KeY;
	
	_current.push(result);
}

void CopyAstVisitor::visit(wptr<TypeType> node) {
	assert(node);
	
	sptr<TypeType> result = TypeType::construct();
	result->location = node->location;
	
	_current.push(result);
}

void CopyAstVisitor::visit(wptr<FunctionDeclaration> node) {
	assert(node);
	
	sptr<FunctionDeclaration> result = FunctionDeclaration::construct();
	result->location = node->location;
	
	result->type = get_copy_of(node->type);
	
	result->name = get_copy_of(node->name);
	
	foreach (wptr<Identifier> id, node->parameterNames)
		result->parameterNames.push_back(get_copy_of(id));
	
	foreach (wptr<Identifier> ttn, node->templateTypeNames)
		result->templateTypeNames.push_back(get_copy_of(ttn));
	
	result->ensurance = node->ensurance;
	
	foreach (wptr<VariableDeclaration> decl, node->logicalVars)
		result->logicalVars.insert(get_copy_of(decl));
	
	foreach (wptr<AssertionArea> pre, node->pre)
		result->pre.insert(get_copy_of(pre));
	
	foreach (wptr<AssertionArea> post, node->post)
		result->post.insert(get_copy_of(post));
	
	result->KeY = node->KeY;
	
	foreach (wptr<CompoundStatement> body, node->body)
		result->body.insert(get_copy_of(body));
	
	_current.push(result);
}

void CopyAstVisitor::visit(wptr<FunctionCall> node) {
	assert(node);
	
	sptr<FunctionCall> result = FunctionCall::construct();
	result->location = node->location;
	
	result->base = get_translation_of_expression(node->base);
	
	foreach (wptr<Expression> expr, node->parameters)
		result->parameters.push_back(get_translation_of_expression(expr));
	
	_current.push(result);
}

void CopyAstVisitor::visit(wptr<OperatorCall> node) {
	assert(node);
	
	sptr<OperatorCall> result = OperatorCall::construct();
	result->location = node->location;
	
	result->op = node->op;
	
	foreach (wptr<Expression> expr, node->operands)
		result->operands.push_back(get_translation_of_expression(expr));
	
	_current.push(result);
}

void CopyAstVisitor::visit(wptr<Reference> node) {
	assert(node);
	
	sptr<Reference> result = Reference::construct();
	result->location = node->location;
	
	if (node->scopePart)
		result->scopePart = get_copy_of(node->scopePart);
	
	if (node->namePart)
		result->namePart = node->namePart;
	
	if (node->formalTypeSpec) {
		result->formalTypeSpec = vector<sptr<Type> >();
		foreach (wptr<Type> type, *node->formalTypeSpec)
			result->formalTypeSpec->push_back(get_translation_of_type(type));
	}
	
	if (node->templateTypeSpec) {
		result->templateTypeSpec = vector<sptr<Type> >();
		foreach (wptr<Type> type, *node->templateTypeSpec)
			result->templateTypeSpec->push_back(get_translation_of_type(type));
	}
	
	_current.push(result);
}

void CopyAstVisitor::visit(wptr<BooleanLiteral> node) {
	assert(node);
	
	sptr<BooleanLiteral> result = BooleanLiteral::construct(node->value);
	result->location = node->location;
	
	_current.push(result);
}

void CopyAstVisitor::visit(wptr<IntegerLiteral> node) {
	assert(node);
	
	sptr<IntegerLiteral> result = IntegerLiteral::construct(node->value);
	result->location = node->location;
	
	_current.push(result);
}

void CopyAstVisitor::visit(wptr<ChainExpression> node) {
	assert(node);
	
	sptr<ChainExpression> result = ChainExpression::construct();
	result->location = node->location;
	
	result->operators = node->operators;
	
	foreach (wptr<Expression> expr, node->operands)
		result->operands.push_back(get_translation_of_expression(expr));
	
	_current.push(result);
}

void CopyAstVisitor::visit(wptr<FunctionType> node) {
	assert(node);
	
	sptr<FunctionType> result = FunctionType::construct();
	result->location = node->location;
	
	result->returnType = get_translation_of_type(node->returnType);
	
	foreach (wptr<Type> type, node->parameterTypes)
		result->parameterTypes.push_back(get_translation_of_type(type));
	
	_current.push(result);
}

void CopyAstVisitor::visit(wptr<PointerType> node) {
	assert(node);
	
	sptr<PointerType> result = PointerType::construct();
	result->location = node->location;
	
	result->type = get_translation_of_type(node->type);
	
	result->strength = node->strength;
	
	_current.push(result);
}

void CopyAstVisitor::visit(wptr<ArrayType> node) {
	assert(node);
	
	sptr<ArrayType> result = ArrayType::construct();
	result->location = node->location;
	
	result->type = get_translation_of_type(node->type);
	
	_current.push(result);
}

void CopyAstVisitor::visit(wptr<NamedType> node) {
	assert(node);
	
	sptr<NamedType> result = NamedType::construct();
	result->location = node->location;
	
	result->reference = get_copy_of(node->reference);
	
	_current.push(result);
}

void CopyAstVisitor::visit(wptr<VoidType> node) {
	assert(node);
	
	sptr<VoidType> result = VoidType::construct();
	result->location = node->location;
	
	_current.push(result);
}

void CopyAstVisitor::visit(wptr<Identifier> node) {
	assert(node);
	
	sptr<Identifier> result = Identifier::construct(node->text);
	result->location = node->location;
	
	_current.push(result);
}

template <class T>
sptr<T> CopyAstVisitor::get_copy_of(wptr<T> node) {
	node->accept(wptr_this());
	sptr<T> result = _current.top().cast<T>();
	_current.pop();
	return result;
}

template <class T>
sptr<T> CopyAstVisitor::get_copy_of(sptr<T> node) {
	return get_copy_of(wptr<T>(node));
}

sptr<Expression> CopyAstVisitor::get_translation_of_expression(wptr<Expression> node) {
	if (typeid(*node) == typeid(Reference)) {
		map<wptr<Symbol>, sptr<Node> >::iterator it = _replacements.find(node.cast<Reference>()->symbol());
		if (it != _replacements.end())
			return it->second.cast<Expression>();
	}
	
	return get_copy_of(node);
}

sptr<Type> CopyAstVisitor::get_translation_of_type(wptr<Type> node) {
	if (typeid(*node) == typeid(NamedType)) {
		map<wptr<Symbol>, sptr<Node> >::iterator it = _replacements.find(node.cast<NamedType>()->reference->symbol());
		if (it != _replacements.end())
			return it->second.cast<Type>();
	}
	
	return get_copy_of(node);
}
